nLab weak excluded middle

Definition

In logic, the principle of weak excluded middle says that for any proposition $P$ we have $\neg P \vee \neg\neg P$.

This follows from the full principle of excluded middle, which says that for any $Q$ we have $Q \vee \neg Q$ (take $Q = \neg P$). Thus, in classical mathematics weak excluded middle is just true. But in constructive mathematics (i.e. intuitionistic logic), it is a weaker assumption than full excluded middle.

Equivalent forms

De Morgan’s Law

In intuitionistic logic, de Morgan’s law often refers to the one of de Morgan's four laws that is not an intuitionistic tautology, namely $\neg (P \wedge Q) \to (\neg P \vee \neg Q)$ for any $P,Q$.

Theorem

De Morgan’s law is equivalent to weak excluded middle.

Proof

If de Morgan’s law holds, then since $\neg (P \wedge \neg P)$, we have $\neg P \vee \neg\neg P$, as desired. Conversely, if weak excluded middle holds and we have $\neg (P\wedge Q)$, then from weak excluded middle we get $\neg P \vee \neg\neg P$ and $\neg Q \vee \neg\neg Q$ which give four cases. In three of those cases $\neg P \vee \neg Q$ holds, while in the fourth we have $\neg\neg P$ and $\neg\neg Q$, which together imply $\neg\neg(P\wedge Q)$ (see the first lemma here and its proof), contradicting the assumption of $\neg (P\wedge Q)$; so the fourth case is impossible.

 See also

• De Morgan's law

• De Morgan Heyting algebra

• De Morgan Heyting category